from __future__ import print_function
from hashlib import *
from z3 import *

def print_stack(stack):
    print('\033[90m------------------------------------- STACK -------------------------------------')
    for s in stack[::-1]:
        if 'z3' in s:
            if is_bv_value( simplify(s['z3'])): print('%10s : %4x  : %x' % (s['type'],s['step'],simplify(s['z3']).as_long() ) )
            else: print('%10s : %4x  : %s' % (s['type'],s['step'], simplify(s['z3']) ) )
        else:
            print('%10s : %4x  ' % (s['type'],s['step']) )
    print('\033[0m')
def get_hash(txt):
    k = md5()
    k.update(txt.encode('utf-8'))
    return int(k.hexdigest(),16)
